the_es:ES, j:E. first(j)  (pred(j) <loc j) 

latex

Definitions	x:A. B(x), P & Q, P  Q, E, t  T, first(e), b, A, (e <loc e'), ES
Lemmas	event system wf, es-axioms, not wf, assert wf, es-first wf, es-E wf